(set-logic QF_LRA)
(declare-fun a () Bool)
(declare-fun b () Bool)
(assert (=> a b))
(check-sat)
(push 1)
(assert (=> a (not b)))
(assert (=> (not a) (not b)))
(assert (=> (not a) b))
(check-sat)
(pop 1)
(check-sat)
(assert (=> a (not b)))
(assert (=> (not a) (not b)))
(assert (=> (not a) b))
(push 1)
(check-sat)
(pop 1)
(check-sat)
